L:Id List, ds, init:Top, i:Id.
([[xL.@i x initially init(x):ds(x)]](i))
~
mk-ma(reduce(x,f. x : ds(x)  f;;L);
;
reduce(x,f. x : init(x)  f;;L);
;
;
;
;
;
;
;
) 

latex

Definitions	x:A. B(x), Top, [[R]], mk-ma, reduce(f;k;as), f  g, x : v, , x. t(x), t  T, , A  B, @i: x:T initially x = v, Y, M1  M2, 1of(t), if b t else f fi, x : t initially x = v, 2of(t), P  Q, true, Prop, as @ bs, filter(P;l), x  dom(f), f(x)?z, f(x), deq-member(eq;x;L), false, x(s), , Unit, P  Q, P & Q, A, False, , , a = b
Lemmas	Rall-nil, Id wf, top wf, Rall-cons, eq id wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff